Step of Proof: mul_cancel_in_eq
12,41
postcript
pdf
Inference at
*
1
1
1
I
of proof for Lemma
mul
cancel
in
eq
:
1.
a
:
2.
b
:
3.
m
:
4. (
m
*
a
) = (
m
*
b
)
5. (
a
>
b
)
(
a
=
b
)
(
a
<
b
)
a
=
b
latex
by RepeatOrHD 5
latex
1
:
1:
5.
a
>
b
1:
a
=
b
2
:
2:
5.
a
=
b
2:
a
=
b
3
:
3:
5.
a
<
b
3:
a
=
b
.
Definitions
P
Q
origin